int_1_intro 12,41
Definitions of inequality predicates on integers and
common integer subtypes. 

Also includes induction lemmas for naturals, and
experiment proving theorem with Ycombinator extract. 

origin